| Definitions | t  T,  x:A. B(x), w.T, f(a), x:A  B(x), S  T, vartype(i;x), locl(a), rcv(l,tg), inr(x), Knd, Id, S  T, inl(x), Msg(M), Msg, x:A B(x), IdLnk, w.M, Type, if b t else f fi, Unit, w.TA, left+right, s = t, Prop, True, P   Q, type List,  A, P & Q, False, outr(x),  b,  b,  , a = b, P  Q, es-V(es), es-M(es), act(k), tag(k), lnk(k), isrcv(k), islocal(k), kindtype(i;k), kindcase(k; a.f(a); l,t.g(l;t) ), Msg, w-kindtype(TA;M;i), w-automaton(T;TA;M), w-machine(w;i), w-machine-independent(w;i;k;x), hasloc(k;i),  x.A(x), <a,b>,  , product-deq(A;B;a;b), E, #$n, A B, a<b, Void,  , {x:A| B(x) }, (x l), KindDeq, deq-member(eq;x;L), P Q, {T}, f(x), x dom(f), z != f(x) P(a;z), M.rframe(k reads x), MsgA, , A & B, mk-ma, x : v, f(x)?z, only members of L read x, M.ds(x), M.bframe(k sends on l), M(i), @i: only members of L read x, M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s,v), M.init(x,v), PossibleWorld(D;w), es-T(es), es-Choose(es), es-Send(es), es-Trans(es), vartype(i;x), Choose(i), Send(i), s1  s2 mod x@i, Trans(i), es-independent(es;i;k;x), ES(the_w), FairFifo, World, D realizes2 es.P(es), es is an event system of D, ES, x. t(x), D realizes es. P(es) |